Section: New Results

Reasoning and programming with infinite data

Participants : Amina Doumane, Yann Régis-Gianas, Alexis Saurin.

This theme is part of the ANR project Rapido (see the National Initiatives section).

Proof theory of infinitary and circular proofs

In collaboration with David Baelde, Amina Doumane and Alexis Saurin developed further the theory of infinite proofs. In their study of the proof theory of circular and infinitary proofs in $\mu MALL$, they established two fundamental proof-theoretical and computational results, namely cut-elimination and focalisation. This result appeared in CSL 2016 (long version in [33]).

The usual result of focalisation for linear logic can actually be extended to circular proofs, but, contrarily to finitary $\mu MALL$ proofs where fixed-points operators can be given an arbitrary polarity, the least fixed-points must be set to be a positive construction and the greatest fixed-points to be negative, which is consistent with intuition from programming with inductive and co-inductive datatypes. An interesting phenomenon arising with focalisation is that some infinite but regular proofs may not have any regular focused proofs. This is similar to what happens for cut-elimination of regular proofs.

The proof of cut-elimination is quite involved and proceeds in two steps relying on semantic arguments, even though the paper actually proves a cut-elimination result and not only a cut-admissibility result as usual semantic arguments provide. A first part of the proof shows that some cut-reduction strategy is actually productive while a second part of the proof shows that the proof-object produced is actually a correct proof in the sense that it satisfies the validity condition of $\mu MALL$ infinite proofs. Previous cut-elimination results were only known for the restricted additive fragment of linear logic with fixed points, a result due to Santocanale and Fortier.

Baelde, Doumane and Saurin are currently working with Jaber to extend the cut-elimination result to a more expressive validity condition for $\mu MALL$ infinite proofs.

Automata theory meets proof theory: proof certificates for Büchi inclusion

In a joint work with David Baelde and Lucca Hirschi, Amina Doumane and Alexis Saurin carried out a proof-theoretical investigation of the linear-time $\mu$-calculus, proposing well-structured proof systems and showing constructively that they are complete for inclusions of Büchi automata suitably encoded as formulas.

They do so in a way that combines the advantages of two lines of previous work: Kaivola gave a proof of completeness for an axiomatisation that amounts to a finitary proof system, but his proof is non-constructive and yields no reasonable procedure. On the other hand, Dax, Hofmann and Lange recently gave a deductive system that is appropriate for algorithmic proof search, but their proofs require a global validity condition and do not have a well understood proof theory.

They work with well-structured proof systems, effectively constructing proofs in a finitary sequent calculus that enjoys local correctness and cut elimination. This involves an intermediate circular proof system in which one can obtain proofs for all inclusions of parity automata, by adapting Safra's construction. In order to finally obtain finite proofs of Büchi inclusions, a translation result from circular to finite proofs is designed.

These results appeared in LICS 2016 (long version in [37]). Since then, Doumane extended the result and obtained a constructive proof of completeness for the full linear-time $\mu$-calculus.

Co-patterns

In collaboration with Paul Laforgue (Master 1, University Paris Diderot), Yann Régis-Gianas studied the mechanisms of co-patterns introduced by Abel and Pientka from a programming language perspective. More precisely, they defined an untyped version of this calculus as well as an abstract machine to efficiently evaluate cofunctions. In addition, they designed several (type preserving) encodings of co-patterns using generalized algebraic datatypes and purely functional objects. Finally, they started to revisit an optimisation called "stream fusion" in a purely equational way by application of copattern-based program definitions.

Functional reactive programming

In collaboration with Sylvain Ribstein (Master 1, University Paris Diderot), Yann Régis-Gianas defined an OCaml library for differential functional reactive programming (DFRP). This framework extends standard functional reactive programming with the possibility to modify past events and to compute the consequences of this modification in all the events that depend on it. A paper is in preparation.

Saurin and Tasson co-advised in the spring/summer of 2016 the master internship of Rémi Nollet who started his PhD thesis under their supervision in September 2016. The topic of his thesis is the extension of Curry-Howard correspondence between FRP and LTL as recently noticed by Jeffrey and Jeltsch. During his internship, Nollet studied various proof systems for LTL and compared them to type systems for FRP. He notably studied various translations between natural deduction and sequent calculus, which led him to study precisely the role played by structural rules in those translations and preparing the work for future extensions to classical constructive LTL, and to work out the foundations for an extension of Curien-Herbelin's system L, closer to abstract machines, for LTL.